COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00012 00003
C00019 00004	In  particular we can assume that the LISP primitives have
C00029 00005	To describe the evaluation of a function-call in LISP we must add
C00034 00006	.NEXT PAGE
C00048 ENDMK
C⊗;

We have borrowed heavily (but informally) from mathematics and logic; we should
at least see how much of our discussion can stand more formal analysis. We
have used the language of functions and functional composition, but have
noted that not all LISP expressions are to be given a usual mathematical connotation.
In particular, conditional expressions are %2not%* to be interpreted as functional
application. 

Most of the description of LISP which we have given so far is classified as ⊗→operational↔←.
That means our informal description of LISP and our later description of the LISP
interpreter are couched in terms of "how does it work  or operate". Indeed
the whole purpose of %3eval%* was to describe explicitly what is to happen
when a LISP expression is to be evaluated.  We have seen ({yon(P84)}) that discussion
of evaluation schemes is non-trivial; and that order of evaluation can effect the
outcome ({yon(P17)}).  
.BEGIN TURN ON "#";
.P91:
However, many times the order of evaluation is immaterial
⊗↓One difficulty with the operational approach is that it (frequently)
specifies too much: C. Wadsworth.←. 
We saw on {yon(P93)} that %3eval%* will perform without complaint when
given a form %3f[#...#]%* supplied with too many arguments.
How much of %3eval%* is "really" LISP and how much is "really" implementation.
On one hand we have said that the meaning of a LISP expression %2is%*
(by#definition) what %3eval%* will do to it. On the other hand
it is quite reasonable to claim %3eval%* is simply %2an implementation%*.
There are certainly other implementations; i.e, other functions %3eval%4i%1
which have the same input-output behavior as our %3eval%*. 
The position here is not that %3eval%* is wrong in giving
values to things like %3cons[A;B;C]%*, but rather: just what is it that
%3eval%* implements?

This other way of looking at meaning in programming languages is exemplified by
⊗→denotational↔← or mathematical semantics.
.P96:
This perspective springs from a common mathematical, philosophical, or logical
device of distinguishing between a %2representation%* for an object, and the
object itself. The most usual guise is the numeral-number distinction.
Numerals are notations (syntax) for talking about %2numbers%* (semantics).
thus the Arabic %2numerals%* %32, 02%*, the Roman numeral %dII%*,
and the Binary notation %310%*, all %2denote%* or represent
the %2number%* two. In LISP, %3(A#B), (A#.(B)), (A,B)%* and %3(A#.(B#.#NIL))%*
all are notations for the same symbolic expression, thought of as an abstract object.
We could say that a LISP form %2denotes%* an S-expr or is undefined  just
as we say in mathematics that 2+2 denotes 4 or 1/0 is undefined. 

Similarly, we will say that
the denotational counterpart of a LISP function  is just a 
 mathematical  function  defined over our abstract domain.
Before  proceeding, discretion dictates the introduction of some conventions
to distinguish notation from %2de%*notation. 
.BEGIN GROUP;
We will continue to use italics:
.BEGIN CENTER;

(%3A, B, ..., x, ... car, ...(A . B) %*) as notation in LISP expressions.
.END
Gothic bold-face:
.BEGIN CENTER;

(%dA, B, ..., x, ...car, ...(A . B)%*) will represent denotations.
.END
.END

Thus %3A%* is notation for %dA%*;
%3car[cdr[(A#B)]]%* denotes %dB%*; the mapping, %dcar%* is the denotation
of the LISP function %3car%*.


The operation of composition of LISP functions tries to denote 
mathematical composition;
thus in LISP, %3car[cdr[(A#B)]]%*  means apply the procedure %3cdr%* to the
argument %3(A#B)%* getting %3(B)%*; apply the procedure %3car%* to %3(B)%*
getting %3B%*. Mathematically speaking, we have a mapping, %dcar%fo%*cdr%1
which is a composition of the %dcar%* and %dcdr%* mappings; the ordered
pair %d<(A#B)#,#B>%* is in the graph of this composed mapping.
%dcar%fo%*cdr(#(A#B)#)%1 is %dB%*.
In this setting, any LISP characterization of a function is equally good;
the "efficiency" question has been abstracted
away. But notice that many important properties of real programs %2can%*  be 
discussed in this  mathematical context; 
in particular, questions of equivalence
and correctness of programs are more approachable.

We should point out that
denotational thinking %2has%* been introduced before.
When we said ({yon(P86)}) that:

.BEGIN CENTERIT;SELECT 3;
←f[a%41%*; ... a%4n%*] = eval[(F A%41%* ... A%4n%*) ...],
.END;
we are 
relating a operational notion with a denotational
notion. The left hand side of this equation
is denotational; the right hand side is operational.
This denotational-operational distinction is appropriate in a more general context.
When we are presented with someone's program and asked "what does it compute?"
we usually begin our investigation operationally, discovering "what does it %2do%*?".
⊗↓Another common manifestation of this "denotation" phenomonon is the common
programmer complaint: "It's easier to write your own than to understand
someone else's."←
Frequently by tracing its execution we can discover a concise (denotational) description
(E.g.,#"ah!#it#computes#the#square#root.").
.END

When %3great mother%* was presented it was given as an operational exercise,
with the primary intent to introduce the LISP evaluation process without
involving the stigma of complicated names. Forms involving %3great mother%* were 
evaluated perhaps without understanding the denotation, but if asked "what does
%3great mother%* do?" you would be hard pressed to given a comprehensible
purely operational definition. However, you might have discovered the intended
nature of %3great mother%* yourself; then it would be relatively easy to describe
its (her) behavior. Indeed, once the denotation of %3great mother%* has been discovered
questions like "What is the value of %3tgmoaf[(CAR#(QUOTE#(A#.#B)))]%*? " 
are usually
answered by using the denotation of %3tgmoaf%*: "what is 
the value of %3car[(A#.#B)]%*?"
The question of how one gives a convincing argument that 
%3eval%* %2does%1 faithfully represent LISP evaluation is the
subject of ⊗↑[Gor#73]↑.


We will parallel  our development of interpreters for LISP since each subset,
%3tgmoaf, tgmoafr%*, and %3eval%*,
will also introduce new problems for our mathematical semantics.

Our first LISP subset considers functions, compostion, and constants.
Constants will be elements of our domain of interpretation.
Our domain will include
the S-expressions since %2most%* LISP expressions %2denote%* Sexprs, and since
 many of our LISP functions are partial functions, 
it is convenient to talk about the undefined value, %9B%1. In other words we
wish to extend our partial functions  to be %2total%* functions on
an extended domain.
As before ({yon(P251)}),
we shall call this extended domain %aS%1.

Before we can talk very precisely about the  properties 
mathematical functions denoted by LISP functions,
we must give more careful study to the nature of domains.
Now of our primitive domains
is  %d<atom>%*.
It's intuitive structure is quite simple, basically just a set of atoms
or names with no inherent relationships  among the elements.
Another primitive domains is %aTr%1, the domain of truth values.

The domain %d<sexpr>%*   is more complex; it is  a set of elements, but many
elements are  related. 
In our discussion of %d<sexpr>%* beginning on {yon(P47)}
we tried to make it clear that there is more than syntax involved.
We could say that
for %ds%41%1 and %ds%42%1 in %d<sexpr>%* then the essence of "dotted pair"
is contained in the concept of the set-theoretic ordered pair, 
<%ds%41%1,%ds%42%1>. Thus the "meaning" of  the set of dotted pairs is
captured by Cartesian product, %d<sexpr>#%ax%*#<sexpr>%1.

.GROUP;
Let's continue the analysis of:

.BEGIN CENTERIT;
←<sexpr> ::= <atom> | (<sexpr> . <sexpr>)
.END
.APART

We are trying to interpret this BNF equation as a definition of the
domain %d<sexpr>%*. Reasonable interpretations of "::=" and "|" appear to
be equality and set-theoretic union, respectively. This results in the
equation:

.BEGIN CENTERIT;SELECT d;
←<sepxr> = <atom> %a∪%* <sexpr> %ax%* <sexpr>
.END

This looks like an algebraic equation, and as such,
may or may not have  solutions.
This "domain equation" has a solution: the S-exprs.

There is a natural mapping of BNF equations onto such "domain equations",
and the solutions to the domain equations are sets satisfying 
the abstract essence of the BNF. 
The recent studies by D. Scott and C. Strachey
study the behavior of such equations, and give existence conditions for
solutions for such equations.

Consider the following BNF:
.BEGIN CENTERIT;
←<wfe> ::= <variable> | %9λ%*<variable>%d.%*<wfe> |  %d(%*<wfe> <wfe>%d)%*
.END
This is an abbreviated form of the BNF for  the %9λ%1-calculus.
We would like to describe the denotations of these equations in a
style similar to that used for <sexpr>'s.
The  denotations of the expressions, <wfe>,
 of applications, %d(%1<wfe>#<wfe>%d)%1, and of the  variables,
<variables>, are just constants of the language; call this domain %dC%*.

Expressions of the form "%9λ%1<variable>%d.%1<wfe>" are supposed to represent
functions. First we consider 
 the set of functions from %dC%* to %dC%*. Write that set as
%dC#→#C%*. Then our domain equation is expressed:

.BEGIN CENTERIT;SELECT d;

←C = C→C
.END
This equation has
no %2interesting%1 solutions. A simple counting argument will establish that 
unless the domain %dC%* is a single element, then the number of functions
in %dC#→#C%* is greater than the number of elements in %dC%*.
This does %2not%1 say that there are no models of the λ-calculus.
It  says is that our interpretation of "%d→%*"
is too broad. 

What is needed is an interpretation of functionality
which will allow a solution to the above domain equation; indeed it
should allow a natural interpretation such that the properties which
we expect functions to posses are, in fact, true in the model.
Scott gave one such 
interpretation of "%d→%*" delimiting  what he calls
 the class of "continuous functions".
This class of functions is restricted enough to satisfy the requirements for
formal study, but broad enough to act as the denotations of procedures in
applicative programming languages.
We will use the notation  "%d[%1D%41%1#%d→%1#D%42%d]%1" to mean " the set of
continuous functions from domain D%41%1 to domain D%42%1.

In  particular we can assume that the LISP primitives have
denote specific continuous functions. For example, the
mathematical counterpart to the LISP function %3car%* is the mapping %dcar%* from 
%aS%* to %aS%* defined as follows:

.BEGIN TABIT2(10,20);GROUP


\%dcar: [%aS%d → %*S%1]

\\ %1| is %9B%* if %dt%* is atomic
\%dcar(t)\%1< %dt%41%1 if %dt%* is %d(t%41%* . t%42%*)
\\ %1| is %9B%* if %dt%* is %9B%*.

.END
Similar strategy suffices to give denotations for the other primitive LISP functions
and predicates. For example: 

.BEGIN TABIT2(10,20);GROUP


\%datom: [%aS%d → %*S%1]

\\ %1| is %ef%* if %dt%* is not atomic.
\%datom(t)\%1< is %et%* if %dt%* is atomic.
\\ %1| is %9B%* if %dt%* is %9B%*.

.END


Corresponding to %3tgmoaf%*, we will have a function, %9D%4tg%1, mapping expressions
onto their denotations.
Since  %9D%4tg%1 is  another mapping like  %9r%1, we will
use the  "%f(%1" and "%f)%1" brackets to enclose LISP constructs
We need to introduce some notation for
elements of the sets <sexpr> and <form>. Let %as%* range over <sexpr>
and %af%* range over <form>, then 
we can write:

.BEGIN centerit;GROUP;

←%9D%4tg%f(%as%f)%1 = %ds%*
←%9D%4tg%f(%3car[%af%*]%f)%1 = %dcar%*(%9D%4tg%f(%af%f)%1)

←with similar entries for %3cdr, cons, eq, %1and %*atom%*.
.END

The structure of this definition is very similar to that of %3tgmoaf%1.
Notice too  that these definitions of the mathematical functions are
strict#({yon(P183)}).

Let's now continue with the next subset of LISP, adding conditional
expressions to our discussion. As we noted on {yon(P88)}, a degree of care need
be taken if we attempt to interpret conditional expressions in terms of mappings.
First we simplify the problem slightly; it is easy to show that a general
LISP conditional can be expressed in terms of the more simple 
%3if%1-expression,
%3if[p%41%*;e%41%*;e%42%*]%1.
We wish to display a denotation for such %3if%1 expressions. It
will be a mathematical function, and thus evaluation order will have been
abstracted out⊗↓%1Recall the comment of Wadsworth
({yon(P91)}). Indeed, the use of conditional expressions in the more
abstract representations of LISP functions frequently is such that 
exactly one of the p%4i%*'s is %et%* and all the others are %ef%*.
Thus in this setting, the order of evaluation of the predicates is useful 
for "efficiency" but not necessary to maintain the sense of the definition.
See {yon(P101)}.←.
Consider 
%3if[p%41%*;e%41%*;e%42%*]%1 as denoting %dif(p%41%*,e%41%*,e%42%*)%1
where:

.BEGIN TABIT2(10,22);GROUP

\%dif: [%aTr%*x%aS%*x%aS%* → %aS%*]

\\ %1| is%* y %1if%* x %1is%* %et%*
\%dif(x,y,z)\%1< is %dz%1, if %dx%1 is %ef%*.
\\ %1| is %9B%1, otherwise
.END
.GROUP;

This interpretation of conditional expressions is appropriate for LISP; other
interpretations of conditionals are possible. For example:

.BEGIN TABIT2(10,24);GROUP

\%dif%41%*: [%aTr%*x%aS%*x%aS%* → %aS%*]

\\ %1| is%* y %1if%* x %1is%* %et%*
\%dif%41%*(x,y,z)\%1< is %dz%1, if %dx%1 is %ef%*.
\\ %1| is %9B%1 if %dx%* is %9B%* and %dy ≠ z%*
\\ %1| is %dy%1 if %dx%* is %9B%* and %dy = z%*
.END
Notice neither %dif%* or %dif%41%1 are strict mappings.
.APART

.GROUP;

To add %3if%1 expressions to %9D%4tg%1, yielding %9D%4tgr%1
we include:
.BEGIN TABIT1(12);FILL;

\%9D%4tgr%f(%3if[%af%41%3 ; %af%42%3; %af%43%3]%f)%1 =
%dif(%9D%4tgr%f(%af%41%f)%d,%9D%4tgr%f(%af%42%f)%d,%9D%4tgr%f(%af%43%f)%d)%1
.END
.APART


The next consideration is the denotational description of LISP identifiers.
Identifiers in LISP represent either S-exprs or functions.
Thus
an identifier either denotes an object on our domain %aS%1 or denotes a function
object.
Let %aFn%* name the set of continuous functions:#%9S%4n=0%d[%aS%8n%d#→#%aS%d]%1,
and %aId%1 be %d<identifier>%1∪%9B%1.
We know that the value of a LISP <identifier> ({yon(P66)})  depends on the 
current environment. 
We first give
a mathematical representation of environments.
Then we might characterize environments as:
.BEGIN CENTER

%denv%1 is the set of functions: %aId%1 → %aS%1 ∪ %aFn%1.
.END
That is, an element of %denv%* is a function which maps an identifier
either onto a S-expr or onto a function from S-exprs to S-exprs.
This is the essence of the argument used in introducing %3assoc%* ({yonss(P92)}).
Note  that %3assoc[x;l]#=#%dl(x)%1 is another instance of a 
operational-denotational relationship.

.BEGIN TURN OFF "{","}";
Given a LISP identifier, %3x%*, and a member of %denv%*, say 
the function %d{<x,2>,<y,4>}%*, then
%9D%* should map %3x%* onto %d2%*. This is an intuitive way of saying
that %9D%* should map a member of <identifier> onto a %2function%*. This function
will map a member of %denv%* onto an element of %aS%*.
Introducing %ai%* as a meta-variable to range over <indetifier>.
then for %dl#%9ε%d#env%1 we have:

.CENTER;
%9D%f(%ai%f)%d(l)%1#=#%dl(i)%1
.END


The %2meaning%* or denotation of a identifier is a function;
whereas the %2value%* of an identifier is an element of %aS%1∪%aFn%1.

The treatment of identifiers leads directly into the
denotional aspects of function application.
We shall maintain the parallels between evaluation and denotation, by giving
%9D%4e%1 and %9D%4a%1 corresponding to %3eval%* and %3apply%*.
Let %ag%1  be a memeber of <function> and %af%1 be a member of <form>;then
for a given element of %denv%1, %9D%4a%1 maps %ag%1 onto an element of
%aFn%1, and %9D%4e%1 maps %af%1 onto an element of %aS%1.

.BEGIN CENTERit;
For example: ←%9D%4a%F(%3car%f)%d(l)%1 = %dcar%1
.END

.GROUP;
Similar equations hold for the other LISP primitive functions and predicates.
In general, then:
.BEGIN CENTER;

%9D%4a%f(%af%f)%d(l)%1 = %dl(f)%*, where %af%* %9ε %1<function>.
.END
.APART
To describe the evaluation of a function-call in LISP we must add
an equation to %9D%4e%1:
.BEGIN  TABIT1(15);FILL;TURN ON "#";

\%9D%4e%f(%af%1[%as%41%1,#...,%as%4n%1]%f)%d(l)%1#=#
%9D%4a%f(%af%f)%d(l)(%9D%4e%f(%as%41%f)%d(l)%1,#...,%9D%4e%f(%as%4n%f)%d(l))%1
.END
We must also make consistent modifications to the previous clauses of %9D%4tgr%1 to
account for environments.
That is, the value of a constant is independent of the
specific environment in which it is evaluated. 
.BEGIN TURN OFF "{","}";TURN ON "#";center;
%9D%4e%1{%as%*}(%dl%*)#=#%ds%*. 

.END
A similar  modification must be made for
conditional expressions.

Before we get very far in applying functions to values
we must give a mathematical characterization of function definitions.
In this section we will handle
 handle λ-notation without free variables, postponing more complex
cases to {yonss(P90)}.

Assuming the only free variables in %9x%* are among the %3x%4i%*'s
the denotation of %3λ[[x%41%*, ..., x%4n%*] %9x%1] in a specified
environment should be a function 
from %aS%8n%1 to %aS%* such that:
.BEGIN TABIT1(15);FILL;TURN ON "#";

\%9D%4a%f(%3λ[[%av%41%1,#...#%av%4n%1]%as%1]%f)%d(l)%1#=#
%d%9λ%d(x%41%*,#...,#%dx%4n%*)%9D%4e%f(%as%f)%d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1
.END

where λ is the LISP λ-notation and %9λ%* is its mathematical counterpart and
%dv%4i%1 is the denotational counterpart of %av%4i%1.

In more detail:
%9λ%d(x%41%*, ... ,x%4n%*)e(x%41%*, ... ,x%4m%*) %1is a function %df%*: %aS%8n%1 → %aS%* such that:

.BEGIN TABIT1(15);GROUP;

\ | is %de(t%41%*, ... ,t%4n%*) %1if m%c≥%*n and %c∀%*i%dt%4i%1 %c≠%* %9B%1.
%df(t%41%*, ... t%4m%*)  %1\<
\ | is %9B%* otherwise

.END
Also, %d(l#:#<x%41%*,%dv%41%d>,#...,#<x%4n%*,%dv%4n%d>)%1 is a modification
of %dl%* such that each %dv%4i%1 is bound to  the corresponding %dx%4i%1.

.BEGIN TABIT2(20,40);GROUP;
That is:\%d(l#:#<x,v>)%1 is: %9λ%d(v%41%*)%2\if %dv = %9B%* %2then %9B%2 
\\else if %dv%41%* = %9B%2 then %9B%2
\\else if %dv%41%* = x%2 then %dv%2
\\else %dl(v%41%*)%1.

where: %2if%d p%* then %dq%* else %dr%1  is  %dif(p,q,r)%1.
.END

After all this work there really should be a comparable return on
on our investment. An immediate benefit is
clearer understanding of the differences between mathematics and programming
languages and a
 clearer perception of the role of definition and computation.
 It should raise questions about the class of objects called function
and the class of objects called procedures.

We know that the LISP %3label%1 operator is similar to "<=", but
%3label%1 builds a temporary definition, while "<=" modifies the
environment. Programming language constructs which modify the environment
are said to have %2side-effects%1 and  are an instance
of what is called a imperative construct.
The next chapter introduces the procedural aspects of 
imperative constructs and  in {yonss(P90)}
we will investigate some of the mathematical aspects of
"<=" and %3label%1.


.NEXT PAGE;
.<<to raproachment???>>
We can give some insight into the mathematical properites of
%3label%1.
As before, we take our clues from the behavior of %3eval%* and %3apply%*.
In any environment %9D%4a%1 should map %3label[f;g]%* in such a way that the 
denotation of %3f%* is synonymous with that of %3g%*.
That is, %df%* is a mapping satisfying the equation 
%df(t%4i%*,#...,#t%4n%*)#=#%dg(t%4i%*,#...,#t%4n%*)%1.
So:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l)%1.
.END

This will suffice for our current λ-definitions; we need not modify %dl%*
since the name %3f%* will never be used within the evaluation of 
an expression involving %3g%*.

.BEGIN TURN ON "#";
We must be a bit careful.
Our treatment of evaluation of free
variables in LISP (on {yon(P93)} and in {yonss(P77)}) shows that free
variables in a function are to be evaluated when the function is %2activated%*
rather than when
 the function is defined. Thus a λ-definition generally
requires an environment in which to evaluate its free variables.
So its denotation 
should be a mapping like: %denv%*#→#[%aS%8n%1#→#%aS%*] rather than
simply %aS%8n%1#→#%aS%1. This is consistent with our understanding of the
meaning of λ-notation.
It is what %3function%* was attempting to 
describe. 
What we previously have called an ⊗→open function↔← is  of the
form: 
 %aS%8n%1#→#%aS%*.

.END
 This view of λ-notation must change our conception on %denv%* as well.
Given a name for a function in an environment we can expect to receive
a mapping from %denv%* to an element of %aFn%*. That is, for such names:

.BEGIN CENTERIT;
←%denv %1is the set of functions: %aId%1 → [%denv%1 → %aFn%1]
.END

A modification of our handling of %3label%* seems to describe the case 
for recursion:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=#%9D%4a%f(%ag%f)%d(l#:#<f,%9D%4a%f(%ag%f)%d>)%1.
.END

Interpreting this equation operationally, it says: when we apply a %3label%*
expression in an environment it is the same as applying the body of the definition
in an environment modified to  associate the name with its definition.
This is analogous to what the LISP %3apply%* function will do.

Recalling the inadequacy of this interpretation of %3label%* in more
general contexts ({yon(P94)}),
we should perhaps look further for a general reading of %3label%*. Our hint
comes from our interpretation of "<=" as an equality. I.e., recall:

.BEGIN CENTER;SELECT 3;TURN OFF "←";

fact ← %1a solution to the equation:%* f = λ[[x][x=0 → 1; %et%3 → *[x;f[x-1]]]].
.END
What we need is a representation of an "equation-solver" which will
take such an equation and will return  a function
which satisfies that equation. In particular we would like the %2best%* 
solution in the sense that it imposes the minimal structure on the function⊗↓Like 
a free group satisfies the group axioms, but imposes no other
requirements.←.
This request for minimality translates to finding the function which
satisfies the equation, but is least-defined on other elements of the
domain. This discussion of "least" brings in the recent work of D. Scott
and  the intuition behind
this study  again illuminates the distinction
between mathematical meaning (denotational) and manipulative meaning (operational).

Consider the following LISP definition:

.BEGIN CENTER;SELECT 3;

f <= λ[[n][n=0 → 0; %et%3 → f[n-1] + 2*n -1]]
.END

.BEGIN TURN ON "#";
When we are asked what this function is doing, most of us would proceed
operationally; that is, we would begin computing %3f[n]%* for different
values of %3n%* --what#is#%3f[0]?%*,
 what is %3f[1]%1,#...#. It is profitable to look at this process differently:
what we are doing is looking  at a %2sequence%* of functions,
call them %df%4i%1's .
.END

.BEGIN TABIT3(10,16,44);SELECT d;GROUP;TURN OFF "{","}";

\f%40%1 =\%d{<0,%9B%*>,<1,%9B%*>, ... }\%1when we begin, we know nothing.
\%df%41%1 =\%d{<0,0>,<1,%9B%*>, ... }\%1now we know one pair.
\%df%42%1 =\%d{<0,0>,<1,1>, ... }\%1now two
\%df%43%1 =\%d{<0,0>,<1,1>,<2,4>, ... }\%1now three

\ ...\           ...          ...\%dEureka!!
.END

When (if) the sudden realization strikes us that the LISP function is
"really" (denotationally)  %dn%82%1 on the non-negative integers, 
then we may either take
that insight on faith or subject it to proof. The process of discovering
the denotation  can be construed as a limiting process which creates 
the least-defined function satisfying the LISP definition. That is:

.BEGIN CENTER;SELECT d;

%9λ%d((n)n%82%d)%1 = %1least upper bound of%d f%4i%1's;
.END
where %df%4i%1 may also be characterised as:

.BEGIN TABIT1(12);SELECT D;group;

\ %1|%d n%82%1 if %d0%c≤%dn%c≤%di
f%4i%d(n)%1 =\<
\ | %9B%1 if %di%c<%dn

.END

We may think of our "equation-solver" as proceeding in such a manner.
Though it is not at all obvious, such an equation solver
%2does%* exist; it is called the %2⊗→fixed-point operator↔←%* and is 
designated here by %dY%*. We will now give an intuitive derivation of %dY%*.


In terms of our example we want a solution to %df = %9t%d(f)%1, where:

.BEGIN CENTER;
%9t%d(g) = %9λ%d((n) cond(n=0, 0, g(n-1)+2*n-1))%1,
.END

Our previous discussion leads us to believe that
%9λ%d((n)n%82%d) %1for %dn %c≥%d0%1 is the desired solution.

.BEGIN TURN ON "#";

How does this discussion relate to the sequence of functions %df%4i%1?
First, it's important to keep the domains of our various mapping in mind:
%df%*#%9ε%*#Fn and %9t%* is a functional in %aFn%1#→#%aFn%1.
Let's look at the behavior of %9t%* for various 
arguments. The simplest function is the totally undefined function, %9B%*#⊗↓We 
perhaps should subscript %9B%* to distinguish it from previous %9B%*'s.←.


.BEGIN CENTER;
%9t%d(%9B%d) = %9λ%d((n) cond(n=0, 0, %9B%*(n-1)+2*n-1))%1,
.END
but this says %9t%d(%9B%*)%1 is just %df%41%1!
Similarly,
.BEGIN CENTER;
%9t%d(%9t%d(%9B%*))#=#%9λ%d((n) cond(n=0, 0, f%41%*(n-1)+2*n-1))%1,
.END
is just %df%42%1.
Thus, writing %9t%8n%1 for the composition of %9t%1...%9t%1, n times, ⊗↓Define
%9t%80%1 to be the the totally undefined function, %9B%1.← we can say
.BEGIN CENTER;GROUP;

%df%4n%* = %9t%8n%d(%9B%*)%1  or,

%9λ%d((n)n%82%*)%1 = lim%4n=0 → ∞%9t%8n%d(%9B%d)%1.
.END

Or in general the fixed-point of an equation %df = %9t%*(f)%1 satisfies the
relation:

.BEGIN CENTER;

%dY(%9t%*) = lim%4n→∞%9t%8n%d(%9B%d).%1
.END
Thus in summary, %dY%* is a mapping: %d[[%aFn%* → %aFn%*] → %aFn%*]%1
such that if %9t%*#%9ε%d#[%aFn%*#→#%aFn%*]%1 and %df%*#=#%9t%d(f)%1, then
%9t%d(Y(%9t%*))%1#=#%dY(%9t%*)%1 and %dY(%9t%*)%1 is least-defined of any of the solutions
to %df%*#=#%9t%d(f)%1.
.END

So the search for denotations for %3label%* might be better served by:

.BEGIN CENTERIT;FILL;TURN ON "#";
←%9D%4a%f(%3label[%af%1;%ag%1]%f)%d(l)%1#=
#%dY(%9λ%d(h)%9D%4a%f(%ag%f)%d(l%1#:#%d<f,h>))%1.
.END


The characterizations are %2not%* the same. Examination of the
behavior of %9D%4e%f(%3label[car;car][(A#B)]%f)%1 will exhibit a discrepancy.
Which characterization of %3label[f;g]%* is "better"?
The first denotation parallels the behavior of %3eval%* and %3apply%*, applying
%3g%* in a %denv%* modified by  the pair %d<f,g>%*.
The later fix-point characterization says %3label[f;g]%* is a particular
solution the the equation %df#=#g%*. As we have seen, the "meaning" of %3label%*
is better served by this fix-point interpretation. The crucial questions, however,
are: first, are these two  denotations different? 
And which, if either, interpretation is %2correct%*? 
That is, which
characterization has the same %2effect%* as %3eval%* and %3apply%*?

The general question of the correctness of the denotational semantics which we
are developing is the subject of much of M. Gordon's thesis.


The intuitions presented in this section can be made very  precise. 
The natural ordering
of "less defined" exemplified by the sequence of %df%4i%1's: %df%4i%1 is less
defined (or approximates) %df%4j%1, j%c≥%1i, imposes a structure on our domain of functions.
Indeed, a structure can be naturally superimposed on all of our domains.
If we require that some additional simple properties hold on our domains, then
the intuitions of this section can be justified mathematically.

*** ADD MONOTONICITY, CONTINUITY

***** continuations and models for imperatives****